Name Binding
------------

<!--
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.

SPDX-License-Identifier: CC0-1.0
-->

[(Up)](../../README.md#topics) | _See also: [Lambda Calculus](../Lambda%20Calculus/README.md#lambda-calculus), [Theorem Proving](../Theorem%20Proving/README.md#theorem-proving)_

- - - -


### Web resources

[How do real-world proof assistants bind variables and check equality?](https://proofassistants.stackexchange.com/questions/4019/how-do-real-world-proof-assistants-bind-variables-and-check-equality) ★


### Repositories

[mathink/mslambda: Map, Skeleton, Lambda term.](https://github.com/mathink/mslambda) ★ [💭](commentary/Chris%20Pressey.md#mathink-mslambda-map-skeleton-lambda-term)

[bacam/sato-maps-agda](https://github.com/bacam/sato-maps-agda) ★ [💭](commentary/Chris%20Pressey.md#bacam-sato-maps-agda)

[jsiek/abstract-binding-trees: Abstract binding trees (abstract syntax trees plus binders), as a library in Agda](https://github.com/jsiek/abstract-binding-trees) ★ [💭](commentary/Chris%20Pressey.md#jsiek-abstract-binding-trees-abstract-binding-trees-abstract-syntax-trees-plus-binders-as-a-library-in-agda)


### Papers

Foundational Aspects of Syntax (online @ [web.archive.org](https://web.archive.org/web/20240304215325/https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lambda-trees.pdf)) ★ [💭](commentary/Chris%20Pressey.md#foundational-aspects-of-syntax)

Abstract Syntax for Variable Binders (online @ [web.archive.org](https://web.archive.org/web/20240415115853/http://www.lix.polytechnique.fr/~dale/papers/cl2000.pdf)) ★ [💭](commentary/Chris%20Pressey.md#abstract-syntax-for-variable-binders)

A Simple Take on Typed Abstract Syntax in Haskell-like Languages (online @ [tidsskrift.dk](https://tidsskrift.dk/brics/article/view/20169)) ★ [💭](commentary/Chris%20Pressey.md#a-simple-take-on-typed-abstract-syntax-in-haskell-like-languages)

[A Metalanguage for Programming with Bound Names Modulo Renaming](https://www.cl.cam.ac.uk/~amp12/papers/metpbn/metpbn.pdf)

[I am not a Number, I am a Free Variable](http://www.e-pig.org/downloads/notanum.pdf) ★ [💭](commentary/Chris%20Pressey.md#i-am-not-a-number-i-am-a-free-variable)

[A Type and Scope Safe Universe of Syntaxes with Binding](https://pure.strath.ac.uk/ws/portalfiles/portal/114903157/Allais_etal_ICFP2018_A_type_and_scope_safe_universe_of_syntaxes_with_binding.pdf)

[Five Axioms of Alpha-Conversion](https://www.cs.ox.ac.uk/tom.melham/pub/Gordon-1996-FAA.pdf) ★

[Don’t Substitute Into Abstractions (Functional Pearl)](https://benl.ouroborus.net/papers/2016-dsim/lambda-dsim-20160328.pdf)

[Abstract Binding Trees, Dynamics and Statics](https://www.cs.cmu.edu/~rjsimmon/15312-s14/hws/hw1update2-handout.pdf) ★ [💭](commentary/Chris%20Pressey.md#abstract-binding-trees-dynamics-and-statics)

[Viewing λ-terms through Maps](https://www.mathematik.uni-muenchen.de/~schwicht/papers/lambda13/lamtheory8.pdf)

_(in [Lambda Calculus](../Lambda%20Calculus/README.md#lambda-calculus))_ A Lambda Calculus with Naive Substitution (online @ [www.cambridge.org](https://www.cambridge.org/core/journals/journal-of-the-australian-mathematical-society/article/lambda-calculus-with-naive-substitution/2ADB7D36897443688E97F3FEA3A84B64)) [💭](commentary/Chris%20Pressey.md#a-lambda-calculus-with-naive-substitution)

_(in [Term Rewriting](../Term%20Rewriting/README.md#term-rewriting))_ [Combinatory Reduction Systems](https://core.ac.uk/download/pdf/82018757.pdf) ★★ [💭](commentary/Chris%20Pressey.md#combinatory-reduction-systems)

_(in [Term Rewriting](../Term%20Rewriting/README.md#term-rewriting))_ [Matching Power](https://web.archive.org/web/20161022182015/http://rho.loria.fr/data/rta2001.pdf) ★ [💭](commentary/Chris%20Pressey.md#matching-power)

_(in [Term Rewriting](../Term%20Rewriting/README.md#term-rewriting))_ [The Rho Cube](https://link.springer.com/content/pdf/10.1007/3-540-45315-6_11.pdf)